(set-option :produce-unsat-model-interpolants true)
(set-logic QF_BV)
(declare-fun v0 () (_ BitVec 1))
(assert (let ((e1(_ bv3322 13)))
(let ((e2(_ bv0 2)))
(let ((e3(_ bv1044 11)))
(let ((e4 (bvmul e1 ((_ zero_extend 11) e2))))
(let ((e5 (ite (bvsle e2 e2) (_ bv1 1) (_ bv0 1))))
(let ((e6 ((_ zero_extend 9) e3)))
(let ((e7 (ite (bvslt e5 e5) (_ bv1 1) (_ bv0 1))))
(let ((e8 (bvashr ((_ sign_extend 18) e2) e6)))
(let ((e9 ((_ rotate_left 7) e1)))
(let ((e10 (bvlshr ((_ sign_extend 9) e3) e6)))
(let ((e11 (bvudiv ((_ zero_extend 7) e9) e6)))
(let ((e12 ((_ repeat 11) e2)))
(let ((e13 (ite (distinct ((_ zero_extend 18) e2) e8) (_ bv1 1) (_ bv0 1))))
(let ((e14 ((_ repeat 31) e5)))
(let ((e15 (bvneg e10)))
(let ((e16 (bvneg v0)))
(let ((e17 (bvule ((_ sign_extend 7) e4) e10)))
(let ((e18 (bvugt ((_ zero_extend 30) e16) e14)))
(let ((e19 (bvugt ((_ sign_extend 12) v0) e4)))
(let ((e20 (bvsle e10 e15)))
(let ((e21 (bvslt ((_ sign_extend 19) e16) e11)))
(let ((e22 (bvult e14 ((_ sign_extend 30) e13))))
(let ((e23 (distinct ((_ zero_extend 19) e7) e6)))
(let ((e24 (bvult e14 ((_ sign_extend 30) e16))))
(let ((e25 (bvsle e14 ((_ sign_extend 11) e10))))
(let ((e26 (bvsle e8 e11)))
(let ((e27 (= e3 ((_ zero_extend 10) e13))))
(let ((e28 (bvslt ((_ sign_extend 19) e16) e15)))
(let ((e29 (bvsle ((_ zero_extend 7) e1) e6)))
(let ((e30 (= e10 ((_ zero_extend 7) e4))))
(let ((e31 (bvslt ((_ sign_extend 7) e4) e15)))
(let ((e32 (bvugt e8 e8)))
(let ((e33 (bvult e12 e12)))
(let ((e34 (bvugt e14 ((_ sign_extend 11) e15))))
(let ((e35 (bvslt e6 ((_ sign_extend 9) e3))))
(let ((e36 (bvsge e14 ((_ zero_extend 11) e10))))
(let ((e37 (bvult e10 e6)))
(let ((e38 (bvule e12 ((_ sign_extend 9) e4))))
(let ((e39 (bvugt e4 ((_ zero_extend 12) e7))))
(let ((e40 (bvsle ((_ zero_extend 2) e6) e12)))
(let ((e41 (bvugt e3 ((_ zero_extend 10) e16))))
(let ((e42 (bvslt e1 e1)))
(let ((e43 (bvult e15 e6)))
(let ((e44 (bvugt ((_ sign_extend 18) e2) e8)))
(let ((e45 (distinct e5 e5)))
(let ((e46 (bvslt ((_ zero_extend 7) e1) e15)))
(let ((e47 (bvuge ((_ sign_extend 21) e7) e12)))
(let ((e48 (bvslt ((_ zero_extend 19) v0) e11)))
(let ((e49 (bvsle e1 e9)))
(let ((e50
(and e17 e18 e19 e20 e21
 e22 e23 e24 e25 e26 e27
 e28 e29 e30 e31 e32 e33
 e34 e35 e36 e37 e38 e39
 e40 e41 e42 e43 e44 e45
 e46 e47 e48 e49
)))
(let ((e51 (and e50 (not (= e6 (_ bv0 20))))))
e51
))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat-assuming-model (v0) ((_ bv0 1)))
(get-unsat-model-interpolant)
